COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	useful set theory
C00006 00003	(proof setfacts)
C00007 00004	(proof setfacts)
C00013 ENDMK
C⊗;
;useful set theory
(wipe-out)
(get-proofs allp)
;we will consider only sets of S-expressions
;XV and YV will have the same declaration as X and Y
(proof sets)

;(axiom |∀xv.sexp(xv)|)
;(label simpinfo)

;(axiom |∀x.groundvar(x)|)
;(label simpinfo)

;(decl (xv yv zv) (type: |ground|) (sort: groundvar))
(decl (av bv) (type: |ground→truthval|))
(decl epsilon (type: |ground⊗@av→truthval|) (infixname: ε) (bindingpower: 925))
(define epsilon |∀av xv.xvεav≡av(xv)|)
(label epsilondef)

(axiom |∀av bv.(∀xv.xvεav≡xvεbv)⊃av=bv|)
(label set_extensionality)

(decl intersection (type: |@av⊗@av→@av|)
      (infixname: ∩) (bindingpower: 950) (prefixname: intersection))
(define intersection |∀av bv.av∩bv=λxv.(av(xv)∧bv(xv))|)
(label interdef)

(decl union (type: |@av⊗@av→@av|)
      (infixname: ∪) (bindingpower: 950) (prefixname: union))
(define union |∀av bv.av∪bv=λxv.(av(xv)∨bv(xv))|)
(label uniondef)

(decl inclusion (type: |@av⊗@av→truthval|)
      (infixname: ⊂) (bindingpower: 920) (prefixname: inclusion))
(define inclusion |∀av bv.av⊂bv≡∀xv.av(xv)⊃bv(xv)|)
(label inclusiondef)

(defax emptyset |emptyset=λxv.false|)
(defax emptyp |∀av.emptyp(av)=∀xv.¬av(xv)|)

;the set of occurrences of an S-exp

(decl mkset (type: |ground→@av|))
(define mkset |∀xv.mkset(xv)=(λyv.yv=xv)|)
(label mkset_def)

;the set of members of a list

(decl mklset (type: |ground→@av|))
(define mklset |∀u.mklset(u)=λx.member(x,u)|)
(label mklsetdef)

(proof setfacts)

;fact about mkset and mklset

(axiom |∀u y.member(y,u)⊃mkset(y)⊂mklset u|)
(label mkset_mklset)

(axiom |∀av bv.av⊂bv∧bv⊂av⊃av=bv|)
(label double_inclusion)
(save-proofs set)
(proof setfacts)

;properties of emptyset
(trw |emptyp(emptyset)| (open emptyp emptyset))
;EMPTYP(EMPTYSET)

(trw |∀xv.¬emptyset(xv)| (open emptyset))
;∀XV.¬EMPTYSET(XV)

;mkset_mklset

(trw |∀u.member(y,u)⊃mkset(y)⊂mklset(u)| 
   (open mkset mklset inclusion)(der))
;∀U.MEMBER(Y,U)⊃MKSET(Y)⊂MKLSET(U)

;double inclusion

(ue ((av.av)(bv.bv)) set_extensionality (open epsilon))
;(∀XV.AV(XV)≡BV(XV))⊃AV=BV

(derive |av⊂bv∧bv⊂av⊃av=bv| (*) (open inclusion))